the_w:World, i:Id, a:Action(i). ((isnull(a)))  (val(a)  valtype(i;a)) 

latex

Definitions	x:A. B(x), P  Q, t  T, valtype(i;a), val(a), w-action-dec(TA;M;i), isl(x), w.TA, w.M, t.1, t.2, kindcase(k; a.f(a); l,t.g(l;t) ), kind(a), outr(x), tt, ff, if b then t else f fi , True, islocal(k), act(k), lnk(k), tag(k), b, outl(x), , World, Action(i), A, b, isnull(a), Action(dec), , Unit, Knd, False, P  Q, P & Q, , rcv(l,tg), locl(a)
Lemmas	eq id wf, ldst wf, bool wf, iff transitivity, assert wf, Id wf, eqtt to assert, assert-eq-id, subtype rel self, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, w-isnull wf, w-action wf, world wf